i, j:. ((i = j) = tt  )  (i = j) 

latex

ProofTree

Definitions	, t  T, P  Q, x:A. B(x), P  Q, P & Q, a  b  T , P  Q, P  Q, Dec(P), False, A
Lemmas	btrue wf, eq int wf, bool wf, decidable int equal, eq int eq false, btrue neq bfalse